Search Results

Documents authored by Klin, Bartek

Document
Complete Volume
DOI: 10.4230/LIPIcs.CSL.2023
LIPIcs, Volume 252, CSL 2023, Complete Volume

Authors: Bartek Klin and Elaine Pimentel

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
LIPIcs, Volume 252, CSL 2023, Complete Volume
Cite as

31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 1-718, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@Proceedings{klin_et_al:LIPIcs.CSL.2023,
  title =	{{LIPIcs, Volume 252, CSL 2023, Complete Volume}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{1--718},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023},
  URN =		{urn:nbn:de:0030-drops-174603},
  doi =		{10.4230/LIPIcs.CSL.2023},
  annote =	{Keywords: LIPIcs, Volume 252, CSL 2023, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CSL.2023.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bartek Klin and Elaine Pimentel

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 0:i-0:xviii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CSL.2023.0,
  author =	{Klin, Bartek and Pimentel, Elaine},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{0:i--0:xviii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.0},
  URN =		{urn:nbn:de:0030-drops-174614},
  doi =		{10.4230/LIPIcs.CSL.2023.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CONCUR.2022
LIPIcs, Volume 243, CONCUR 2022, Complete Volume

Authors: Bartek Klin, Sławomir Lasota, and Anca Muscholl

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
LIPIcs, Volume 243, CONCUR 2022, Complete Volume
Cite as

33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 1-712, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@Proceedings{klin_et_al:LIPIcs.CONCUR.2022,
  title =	{{LIPIcs, Volume 243, CONCUR 2022, Complete Volume}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{1--712},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022},
  URN =		{urn:nbn:de:0030-drops-170623},
  doi =		{10.4230/LIPIcs.CONCUR.2022},
  annote =	{Keywords: LIPIcs, Volume 243, CONCUR 2022, Complete Volume}
}
Document
Front Matter
DOI: 10.4230/LIPIcs.CONCUR.2022.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Bartek Klin, Sławomir Lasota, and Anca Muscholl

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)

Abstract
Front Matter, Table of Contents, Preface, Conference Organization
Cite as

33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 0:i-0:x, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CONCUR.2022.0,
  author =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{0:i--0:x},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2022.0},
  URN =		{urn:nbn:de:0030-drops-170631},
  doi =		{10.4230/LIPIcs.CONCUR.2022.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2022.64
Countdown μ-Calculus

Authors: Jędrzej Kołodziejski and Bartek Klin

Published in: LIPIcs, Volume 241, 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)

Abstract
We introduce the countdown μ-calculus, an extension of the modal μ-calculus with ordinal approximations of fixpoint operators. In addition to properties definable in the classical calculus, it can express (un)boundedness properties such as the existence of arbitrarily long sequences of specific actions. The standard correspondence with parity games and automata extends to suitably defined countdown games and automata. However, unlike in the classical setting, the scalar fragment is provably weaker than the full vectorial calculus and corresponds to automata satisfying a simple syntactic condition. We establish some facts, in particular decidability of the model checking problem and strictness of the hierarchy induced by the maximal allowed nesting of our new operators.
Cite as

Jędrzej Kołodziejski and Bartek Klin. Countdown μ-Calculus. In 47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 241, pp. 64:1-64:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{kolodziejski_et_al:LIPIcs.MFCS.2022.64,
  author =	{Ko{\l}odziejski, J\k{e}drzej and Klin, Bartek},
  title =	{{Countdown \mu-Calculus}},
  booktitle =	{47th International Symposium on Mathematical Foundations of Computer Science (MFCS 2022)},
  pages =	{64:1--64:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-256-3},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{241},
  editor =	{Szeider, Stefan and Ganian, Robert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2022.64},
  URN =		{urn:nbn:de:0030-drops-168624},
  doi =		{10.4230/LIPIcs.MFCS.2022.64},
  annote =	{Keywords: countdown \mu-calculus, games, automata}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2021.1
μ-Calculi with Atoms (Invited Talk)

Authors: Bartek Klin

Published in: LIPIcs, Volume 183, 29th EACSL Annual Conference on Computer Science Logic (CSL 2021)

Abstract
Modal μ-calculus is a well-known formalism for describing properties of state-based transition systems. It can define properties such as "[in the current state] p holds, and there is a path where is holds again at some point in the future", where p comes from some fixed vocabulary of basic predicates. A formula of the classical μ-calculus refers only to finitely many basic predicates, which may sometimes seem restrictive. Real systems routinely operate on data coming from potentially infinite domains, such as numbers or character strings. Basic properties of such systems may reasonably include ones like "the number n was input", for every number n. It is then not clear how to say that "there exists a transition path where the currently input number is input again some time in the future" as a formula. Various modal formalisms have been proposed to model temporal properties of systems that refer to data coming from infinite domains. Here I focus on the modal μ-calculus with atoms, which is an extension of the classical calculus with features of nominal sets. There, basic predicates, formulas and models rely on atoms that come from some fixed infinite domain and can be tested for equality (or, in an extended variant, for some fixed order). I present a few variants of the modal μ-calculus with atoms, and describe their properties. As an example application, I show how to formulate the security property of the cryptographic Needham-Schroeder protocol, which relies on generating atomic nonces and comparing them for equality, and which famously fails due to a man-in-the-middle attack. Much of the material presented in this talk is drawn from [C. Eberhart and B. Klin, 2019; B. Klin and M. Łełyk, 2019; B. Klin and M. Łełyk, 2017].
Cite as

Bartek Klin. μ-Calculi with Atoms (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{klin:LIPIcs.CSL.2021.1,
  author =	{Klin, Bartek},
  title =	{{\mu-Calculi with Atoms}},
  booktitle =	{29th EACSL Annual Conference on Computer Science Logic (CSL 2021)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-175-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{183},
  editor =	{Baier, Christel and Goubault-Larrecq, Jean},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2021.1},
  URN =		{urn:nbn:de:0030-drops-134358},
  doi =		{10.4230/LIPIcs.CSL.2021.1},
  annote =	{Keywords: modal \mu-calculus, sets with atoms}
}
Document
DOI: 10.4230/LIPIcs.CSL.2017.30
Modal mu-Calculus with Atoms

Authors: Bartek Klin and Mateusz Lelyk

Published in: LIPIcs, Volume 82, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Abstract
We introduce an extension of modal mu-calculus to sets with atoms and study its basic properties. Model checking is decidable on orbit-finite structures, and a correspondence to parity games holds. On the other hand, satisfiability becomes undecidable. We also show some limitations to the expressiveness of the calculus and argue that a naive way to remove these limitations results in a logic whose model checking is undecidable.
Cite as

Bartek Klin and Mateusz Lelyk. Modal mu-Calculus with Atoms. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 30:1-30:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CSL.2017.30,
  author =	{Klin, Bartek and Lelyk, Mateusz},
  title =	{{Modal mu-Calculus with Atoms}},
  booktitle =	{26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
  pages =	{30:1--30:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-045-3},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{82},
  editor =	{Goranko, Valentin and Dam, Mads},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2017.30},
  URN =		{urn:nbn:de:0030-drops-76991},
  doi =		{10.4230/LIPIcs.CSL.2017.30},
  annote =	{Keywords: modal mu-calculus, sets with atoms}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.105
Expressiveness of Probabilistic Modal Logics, Revisited

Authors: Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.
Cite as

Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of Probabilistic Modal Logics, Revisited. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 105:1-105:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.ICALP.2017.105,
  author =	{Fijalkow, Nathana\"{e}l and Klin, Bartek and Panangaden, Prakash},
  title =	{{Expressiveness of Probabilistic Modal Logics, Revisited}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{105:1--105:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.105},
  URN =		{urn:nbn:de:0030-drops-73683},
  doi =		{10.4230/LIPIcs.ICALP.2017.105},
  annote =	{Keywords: probabilistic modal logic, probabilistic bisimulation, probabilistic simulation}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2016.14
Homomorphism Problems for First-Order Definable Structures

Authors: Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Torunczyk

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
We investigate several variants of the homomorphism problem: given two relational structures, is there a homomorphism from one to the other? The input structures are possibly infinite, but definable by first-order interpretations in a fixed structure. Their signatures can be either finite or infinite but definable. The homomorphisms can be either arbitrary, or definable with parameters, or definable without parameters. For each of these variants, we determine its decidability status.
Cite as

Bartek Klin, Slawomir Lasota, Joanna Ochremiak, and Szymon Torunczyk. Homomorphism Problems for First-Order Definable Structures. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 14:1-14:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.FSTTCS.2016.14,
  author =	{Klin, Bartek and Lasota, Slawomir and Ochremiak, Joanna and Torunczyk, Szymon},
  title =	{{Homomorphism Problems for First-Order Definable Structures}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{14:1--14:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.14},
  URN =		{urn:nbn:de:0030-drops-68498},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.14},
  annote =	{Keywords: Sets with atoms, first-order interpretations, homomorphism problem}
}
Document
DOI: 10.4230/LIPIcs.CALCO.2015.190
Presenting Morphisms of Distributive Laws

Authors: Bartek Klin and Beata Nachyla

Published in: LIPIcs, Volume 35, 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)

Abstract
A format for well-behaved translations between structural operational specifications is derived from a notion of distributive law morphism, previously studied by Power and Watanabe.
Cite as

Bartek Klin and Beata Nachyla. Presenting Morphisms of Distributive Laws. In 6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 35, pp. 190-204, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{klin_et_al:LIPIcs.CALCO.2015.190,
  author =	{Klin, Bartek and Nachyla, Beata},
  title =	{{Presenting Morphisms of Distributive Laws}},
  booktitle =	{6th Conference on Algebra and Coalgebra in Computer Science (CALCO 2015)},
  pages =	{190--204},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-84-2},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{35},
  editor =	{Moss, Lawrence S. and Sobocinski, Pawel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CALCO.2015.190},
  URN =		{urn:nbn:de:0030-drops-55343},
  doi =		{10.4230/LIPIcs.CALCO.2015.190},
  annote =	{Keywords: coalgebra, bialgebra, distributive law, structural operational semantics}
}
Document
DOI: 10.4230/DagRep.3.10.58
Nominal Computation Theory (Dagstuhl Seminar 13422)

Authors: Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts

Published in: Dagstuhl Reports, Volume 3, Issue 10 (2014)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 13422 "Nominal Computation Theory". The underlying theme of the seminar was nominal sets (also known as sets with atoms or Fraenkel-Mostowski sets) and they role and applications in three distinct research areas: automata over infinite alphabets, program semantics using nominal sets and nominal calculi of concurrent processes.
Cite as

Mikolaj Bojanczyk, Bartek Klin, Alexander Kurz, and Andrew M. Pitts. Nominal Computation Theory (Dagstuhl Seminar 13422). In Dagstuhl Reports, Volume 3, Issue 10, pp. 58-71, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{bojanczyk_et_al:DagRep.3.10.58,
  author =	{Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.},
  title =	{{Nominal Computation Theory (Dagstuhl Seminar 13422)}},
  pages =	{58--71},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{3},
  number =	{10},
  editor =	{Bojanczyk, Mikolaj and Klin, Bartek and Kurz, Alexander and Pitts, Andrew M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.3.10.58},
  URN =		{urn:nbn:de:0030-drops-44285},
  doi =		{10.4230/DagRep.3.10.58},
  annote =	{Keywords: nominal sets, Fraenkel-Mostowski sets}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact